\begin{tabbing}
EventsWithKinds
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type\+
\\[0ex]$\times$EqDecider($E$)
\\[0ex]$\times$Top
\\[0ex]$\times$${\it pred?}$:($E$$\rightarrow$($E$+Unit))
\\[0ex]$\times$${\it info}$:($E$$\rightarrow$(Id$\times$Id+(IdLnk$\times$$E$)$\times$Id))
\\[0ex]$\times$EOrderAxioms($E$; ${\it pred?}$; ${\it info}$)
\\[0ex]$\times$$T$:(Id$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$${\it when}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(loc($e$),$x$))
\\[0ex]$\times$${\it after}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(loc($e$),$x$))
\\[0ex]$\times$($\forall$$e$:$E$. $\neg$first($e$) $\Rightarrow$ ($\forall$$x$:Id. ${\it when}$($x$,$e$) $=$ ${\it after}$($x$,pred($e$))))
\\[0ex]$\times$Top
\-
\end{tabbing}